Definitions | x:A. B(x), fpf-cap(f; eq; x; z), fpf-single(x; v), if b then t else f fi , fpf-dom(eq; x; f), fpf-ap(f; eq; x), t.2, deq-member(eq; x; L), t.1, reduce(f; k; as), ff, Y, t T, P  Q, tt, P Q, b, P   Q, prop{i:l}, True, P Q, P  Q,  b, T, , Unit, False, A,  |